Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    p(0)  → 0
2:    p(s(x))  → x
3:    le(0,y)  → true
4:    le(s(x),0)  → false
5:    le(s(x),s(y))  → le(x,y)
6:    minus(x,0)  → x
7:    minus(x,s(y))  → if(le(x,s(y)),0,p(minus(x,p(s(y)))))
8:    if(true,x,y)  → x
9:    if(false,x,y)  → y
There are 6 dependency pairs:
10:    LE(s(x),s(y))  → LE(x,y)
11:    MINUS(x,s(y))  → IF(le(x,s(y)),0,p(minus(x,p(s(y)))))
12:    MINUS(x,s(y))  → LE(x,s(y))
13:    MINUS(x,s(y))  → P(minus(x,p(s(y))))
14:    MINUS(x,s(y))  → MINUS(x,p(s(y)))
15:    MINUS(x,s(y))  → P(s(y))
The approximated dependency graph contains 2 SCCs: {10} and {14}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006